1. $T$ : Type
\\[0ex]2. $a$ : $T$ List
\\[0ex]3. $b$ : $T$ List
\\[0ex]4. $\parallel$$a$$\parallel$ = $\parallel$$b$$\parallel$
\\[0ex]5. $\forall$$i$:$\mathbb{N}$. ($i$ $<$ $\parallel$$a$$\parallel$) $\Rightarrow$ ($a$[$i$] = $b$[$i$])
\\[0ex]$\vdash$  $a$ = $b$